Left Termination of the query pattern
in(a,g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

in(X, tree(X, X1, X2)).
in(X, tree(Y, Left, X3)) :- ','(less(X, Y), in(X, Left)).
in(X, tree(Y, X4, Right)) :- ','(less(Y, X), in(X, Right)).
less(0, s(X5)).
less(s(X), s(Y)) :- less(X, Y).

Query: in(a,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="H: in(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: in(T1, T2), SCOPE: 1, CLAUSE: 0 | in(T1, T2), SCOPE: 1, CLAUSE: 1 | in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: in(T1, T2), SCOPE: 1, CLAUSE: 1 | in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, T2) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(less(T17, T14), in(T17, T15)) | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 3 | ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4 | ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 3\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4 | ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="A: in(0, T15)\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: in(0, T15), SCOPE: 3, CLAUSE: 0 | in(0, T15), SCOPE: 3, CLAUSE: 1 | in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: in(0, T15), SCOPE: 3, CLAUSE: 0\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: in(0, T15), SCOPE: 3, CLAUSE: 1 | in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: in(0, T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(less(0, T49), in(0, T50))\n\nT49 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="B: less(0, T49)\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: in(0, T50)\n\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: less(0, T49), SCOPE: 4, CLAUSE: 3 | less(0, T49), SCOPE: 4, CLAUSE: 4\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: less(0, T49), SCOPE: 4, CLAUSE: 3\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: less(0, T49), SCOPE: 4, CLAUSE: 4\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(less(T71, 0), in(0, T73))\n\nT71 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="C: less(T71, 0)\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: in(0, T73)\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: less(T71, 0), SCOPE: 5, CLAUSE: 3 | less(T71, 0), SCOPE: 5, CLAUSE: 4\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T71, 0), SCOPE: 5, CLAUSE: 4\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="I: ','(less(T89, T88), in(s(T89), T15))\n\nT15 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="D: less(T89, T88)\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="E: in(s(T92), T15)\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: less(T89, T88), SCOPE: 6, CLAUSE: 3 | less(T89, T88), SCOPE: 6, CLAUSE: 4\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: less(T89, T88), SCOPE: 6, CLAUSE: 3\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: less(T89, T88), SCOPE: 6, CLAUSE: 4\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: less(T106, T105)\n\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: in(s(T92), T15), SCOPE: 7, CLAUSE: 0 | in(s(T92), T15), SCOPE: 7, CLAUSE: 1 | in(s(T92), T15), SCOPE: 7, CLAUSE: 2\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: in(s(T92), T15), SCOPE: 7, CLAUSE: 0\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: in(s(T92), T15), SCOPE: 7, CLAUSE: 1 | in(s(T92), T15), SCOPE: 7, CLAUSE: 2\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: in(s(T92), T15), SCOPE: 7, CLAUSE: 1\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: in(s(T92), T15), SCOPE: 7, CLAUSE: 2\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(less(s(T146), T147), in(s(T146), T148))\n\nT146 is ground\nT147 is ground\nT148 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="F: less(s(T146), T147)\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: in(s(T146), T148)\n\nT146 is ground\nT148 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: less(s(T146), T147), SCOPE: 8, CLAUSE: 3 | less(s(T146), T147), SCOPE: 8, CLAUSE: 4\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: less(s(T146), T147), SCOPE: 8, CLAUSE: 4\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="G: less(T154, T155)\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: less(T154, T155), SCOPE: 9, CLAUSE: 3 | less(T154, T155), SCOPE: 9, CLAUSE: 4\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: less(T154, T155), SCOPE: 9, CLAUSE: 3\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: less(T154, T155), SCOPE: 9, CLAUSE: 4\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: less(T167, T168)\n\nT167 is ground\nT168 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(less(T186, s(T185)), in(s(T185), T188))\n\nT185 is ground\nT186 is ground\nT188 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: less(T186, s(T185))\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: in(s(T185), T188)\n\nT185 is ground\nT188 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="J: ','(less(T211, T214), in(T214, T213))\n\nT211 is ground\nT213 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="K: less(T211, T214)\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: in(T217, T213)\n\nT213 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: less(T211, T214), SCOPE: 10, CLAUSE: 3 | less(T211, T214), SCOPE: 10, CLAUSE: 4\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: less(T211, T214), SCOPE: 10, CLAUSE: 3\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: less(T211, T214), SCOPE: 10, CLAUSE: 4\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: less(T229, T231)\n\nT229 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(less(T248, T245), in(T248, T246)) | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, T2) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 3 | ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 4 | ?_11 | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 3\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 4 | ?_11 | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: in(0, T246)\n\nT246 is ground\nT247 is ground\nT253 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T253), T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 4\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ?_11 | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(less(T268, T267), in(s(T268), T246))\n\nT246 is ground\nT247 is ground\nT267 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T267), T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(less(T283, T286), in(T286, T285))\n\nT283 is ground\nT284 is ground\nT285 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T283, T284, T285)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(less(T294, T297), in(T297, T296))\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 3 | ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 4\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 3\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 4\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: in(s(T303), T296)\n\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(0, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(less(T314, T316), in(s(T316), T296))\n\nT295 is ground\nT296 is ground\nT314 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T314), T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: less(T314, T316)\n\nT295 is ground\nT296 is ground\nT314 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T314), T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: in(s(T319), T296)\n\nT295 is ground\nT296 is ground\nT314 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T320, tree(s(T314), T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 116 [arrowhead = none ];
116 -> 2;

117 [label="EVAL with clause\nin(X9, tree(X9, X10, X11)).\nand substitutionT1 -> T6,\nX9 -> T6,\nX10 -> T7,\nX11 -> T8,\nT2 -> tree(T6, T7, T8)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 117 [arrowhead = none ];
117 -> 3;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 118 [arrowhead = none ];
118 -> 4;

119 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 119 [arrowhead = none ];
119 -> 5;

120 [label="EVAL with clause\nin(X271, tree(X272, X273, X274)) :- ','(less(X271, X272), in(X271, X273)).\nand substitutionT1 -> T248,\nX271 -> T248,\nX272 -> T245,\nX273 -> T246,\nX274 -> T247,\nT2 -> tree(T245, T246, T247),\nT244 -> T248", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 120 [arrowhead = none ];
120 -> 92;

121 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 121 [arrowhead = none ];
121 -> 93;

122 [label="ONLY EVAL with clause\nin(X16, tree(X17, X18, X19)) :- ','(less(X16, X17), in(X16, X18)).\nand substitutionT1 -> T17,\nX16 -> T17,\nT6 -> T14,\nX17 -> T14,\nT7 -> T15,\nX18 -> T15,\nT8 -> T16,\nX19 -> T16,\nT13 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 122 [arrowhead = none ];
122 -> 6;

123 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
6 -> 123 [arrowhead = none ];
123 -> 7;

124 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
7 -> 124 [arrowhead = none ];
124 -> 8;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
7 -> 125 [arrowhead = none ];
125 -> 9;

126 [label="EVAL with clause\nless(0, s(X24)).\nand substitutionT17 -> 0,\nX24 -> T22,\nT14 -> s(T22)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 126 [arrowhead = none ];
126 -> 10;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 127 [arrowhead = none ];
127 -> 11;

128 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 128 [arrowhead = none ];
128 -> 38;

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 129 [arrowhead = none ];
129 -> 39;

130 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 130 [arrowhead = none ];
130 -> 12;

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 131 [arrowhead = none ];
131 -> 13;

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 132 [arrowhead = none ];
132 -> 14;

133 [label="EVAL with clause\nin(X43, tree(X43, X44, X45)).\nand substitutionX43 -> 0,\nX44 -> T35,\nX45 -> T36,\nT15 -> tree(0, T35, T36)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 133 [arrowhead = none ];
133 -> 15;

134 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 134 [arrowhead = none ];
134 -> 16;

135 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 135 [arrowhead = none ];
135 -> 18;

136 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 136 [arrowhead = none ];
136 -> 19;

137 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 137 [arrowhead = none ];
137 -> 17;

138 [label="EVAL with clause\nin(X62, tree(X63, X64, X65)) :- ','(less(X62, X63), in(X62, X64)).\nand substitutionX62 -> 0,\nX63 -> T49,\nX64 -> T50,\nX65 -> T51,\nT15 -> tree(T49, T50, T51)", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 138 [arrowhead = none ];
138 -> 20;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 139 [arrowhead = none ];
139 -> 21;

140 [label="EVAL with clause\nin(X91, tree(X92, X93, X94)) :- ','(less(X92, X91), in(X91, X94)).\nand substitutionX91 -> 0,\nX92 -> T71,\nX93 -> T72,\nX94 -> T73,\nT15 -> tree(T71, T72, T73)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 140 [arrowhead = none ];
140 -> 31;

141 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 141 [arrowhead = none ];
141 -> 32;

142 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 142 [arrowhead = none ];
142 -> 22;

143 [label="SPLIT 2\nnew knowledge:\nT49 is ground", fontsize=14, style = filled, fillcolor = violet];
20 -> 143 [arrowhead = none ];
143 -> 23;

144 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 144 [arrowhead = none ];
144 -> 24;

145 [label="INSTANCE with matching:\nT15 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 145 [arrowhead = none , style=dashed];
145 -> 10[style=dashed];

146 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 146 [arrowhead = none ];
146 -> 25;

147 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 147 [arrowhead = none ];
147 -> 26;

148 [label="EVAL with clause\nless(0, s(X74)).\nand substitutionX74 -> T60,\nT49 -> s(T60)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 148 [arrowhead = none ];
148 -> 27;

149 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 149 [arrowhead = none ];
149 -> 28;

150 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 150 [arrowhead = none ];
150 -> 30;

151 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 151 [arrowhead = none ];
151 -> 29;

152 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
31 -> 152 [arrowhead = none ];
152 -> 33;

153 [label="SPLIT 2\nnew knowledge:\nT71 is ground", fontsize=14, style = filled, fillcolor = violet];
31 -> 153 [arrowhead = none ];
153 -> 34;

154 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 154 [arrowhead = none ];
154 -> 35;

155 [label="INSTANCE with matching:\nT15 -> T73", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 155 [arrowhead = none , style=dashed];
155 -> 10[style=dashed];

156 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 156 [arrowhead = none ];
156 -> 36;

157 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 157 [arrowhead = none ];
157 -> 37;

158 [label="EVAL with clause\nless(s(X116), s(X117)) :- less(X116, X117).\nand substitutionX116 -> T89,\nT17 -> s(T89),\nX117 -> T88,\nT14 -> s(T88),\nT87 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 158 [arrowhead = none ];
158 -> 40;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 159 [arrowhead = none ];
159 -> 41;

160 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 160 [arrowhead = none ];
160 -> 80;

161 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 161 [arrowhead = none ];
161 -> 42;

162 [label="SPLIT 2\nnew knowledge:\nT92 is ground\nT88 is ground\nreplacements:T89 -> T92", fontsize=14, style = filled, fillcolor = violet];
40 -> 162 [arrowhead = none ];
162 -> 43;

163 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
42 -> 163 [arrowhead = none ];
163 -> 44;

164 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 164 [arrowhead = none ];
164 -> 52;

165 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 165 [arrowhead = none ];
165 -> 45;

166 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 166 [arrowhead = none ];
166 -> 46;

167 [label="EVAL with clause\nless(0, s(X126)).\nand substitutionT89 -> 0,\nX126 -> T99,\nT88 -> s(T99)", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 167 [arrowhead = none ];
167 -> 47;

168 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 168 [arrowhead = none ];
168 -> 48;

169 [label="EVAL with clause\nless(s(X131), s(X132)) :- less(X131, X132).\nand substitutionX131 -> T106,\nT89 -> s(T106),\nX132 -> T105,\nT88 -> s(T105),\nT104 -> T106", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 169 [arrowhead = none ];
169 -> 50;

170 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 170 [arrowhead = none ];
170 -> 51;

171 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 171 [arrowhead = none ];
171 -> 49;

172 [label="INSTANCE with matching:\nT89 -> T106\nT88 -> T105", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 172 [arrowhead = none , style=dashed];
172 -> 42[style=dashed];

173 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 173 [arrowhead = none ];
173 -> 53;

174 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 174 [arrowhead = none ];
174 -> 54;

175 [label="EVAL with clause\nin(X153, tree(X153, X154, X155)).\nand substitutionT92 -> T127,\nX153 -> s(T127),\nX154 -> T128,\nX155 -> T129,\nT15 -> tree(s(T127), T128, T129)", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 175 [arrowhead = none ];
175 -> 55;

176 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 176 [arrowhead = none ];
176 -> 56;

177 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 177 [arrowhead = none ];
177 -> 58;

178 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 178 [arrowhead = none ];
178 -> 59;

179 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 179 [arrowhead = none ];
179 -> 57;

180 [label="EVAL with clause\nin(X172, tree(X173, X174, X175)) :- ','(less(X172, X173), in(X172, X174)).\nand substitutionT92 -> T146,\nX172 -> s(T146),\nX173 -> T147,\nX174 -> T148,\nX175 -> T149,\nT15 -> tree(T147, T148, T149)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 180 [arrowhead = none ];
180 -> 60;

181 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 181 [arrowhead = none ];
181 -> 61;

182 [label="EVAL with clause\nin(X216, tree(X217, X218, X219)) :- ','(less(X217, X216), in(X216, X219)).\nand substitutionT92 -> T185,\nX216 -> s(T185),\nX217 -> T186,\nX218 -> T187,\nX219 -> T188,\nT15 -> tree(T186, T187, T188)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 182 [arrowhead = none ];
182 -> 76;

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 183 [arrowhead = none ];
183 -> 77;

184 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
60 -> 184 [arrowhead = none ];
184 -> 62;

185 [label="SPLIT 2\nnew knowledge:\nT146 is ground\nT147 is ground", fontsize=14, style = filled, fillcolor = violet];
60 -> 185 [arrowhead = none ];
185 -> 63;

186 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
62 -> 186 [arrowhead = none ];
186 -> 64;

187 [label="INSTANCE with matching:\nT92 -> T146\nT15 -> T148", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 187 [arrowhead = none , style=dashed];
187 -> 43[style=dashed];

188 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 188 [arrowhead = none ];
188 -> 65;

189 [label="EVAL with clause\nless(s(X185), s(X186)) :- less(X185, X186).\nand substitutionT146 -> T154,\nX185 -> T154,\nX186 -> T155,\nT147 -> s(T155)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 189 [arrowhead = none ];
189 -> 66;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 190 [arrowhead = none ];
190 -> 67;

191 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
66 -> 191 [arrowhead = none ];
191 -> 68;

192 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 192 [arrowhead = none ];
192 -> 69;

193 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 193 [arrowhead = none ];
193 -> 70;

194 [label="EVAL with clause\nless(0, s(X193)).\nand substitutionT154 -> 0,\nX193 -> T162,\nT155 -> s(T162)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 194 [arrowhead = none ];
194 -> 71;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 195 [arrowhead = none ];
195 -> 72;

196 [label="EVAL with clause\nless(s(X198), s(X199)) :- less(X198, X199).\nand substitutionX198 -> T167,\nT154 -> s(T167),\nX199 -> T168,\nT155 -> s(T168)", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 196 [arrowhead = none ];
196 -> 74;

197 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 197 [arrowhead = none ];
197 -> 75;

198 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 198 [arrowhead = none ];
198 -> 73;

199 [label="INSTANCE with matching:\nT154 -> T167\nT155 -> T168", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 199 [arrowhead = none , style=dashed];
199 -> 66[style=dashed];

200 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
76 -> 200 [arrowhead = none ];
200 -> 78;

201 [label="SPLIT 2\nnew knowledge:\nT186 is ground\nT185 is ground", fontsize=14, style = filled, fillcolor = violet];
76 -> 201 [arrowhead = none ];
201 -> 79;

202 [label="INSTANCE with matching:\nT154 -> T186\nT155 -> s(T185)", fontsize=14, style = filled, fillcolor = lightgrey];
78 -> 202 [arrowhead = none , style=dashed];
202 -> 66[style=dashed];

203 [label="INSTANCE with matching:\nT92 -> T185\nT15 -> T188", fontsize=14, style = filled, fillcolor = lightgrey];
79 -> 203 [arrowhead = none , style=dashed];
203 -> 43[style=dashed];

204 [label="ONLY EVAL with clause\nin(X240, tree(X241, X242, X243)) :- ','(less(X241, X240), in(X240, X243)).\nand substitutionT1 -> T214,\nX240 -> T214,\nT14 -> T211,\nX241 -> T211,\nT15 -> T212,\nX242 -> T212,\nT16 -> T213,\nX243 -> T213,\nT210 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 204 [arrowhead = none ];
204 -> 81;

205 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
81 -> 205 [arrowhead = none ];
205 -> 82;

206 [label="SPLIT 2\nnew knowledge:\nT211 is ground\nreplacements:T214 -> T217", fontsize=14, style = filled, fillcolor = violet];
81 -> 206 [arrowhead = none ];
206 -> 83;

207 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
82 -> 207 [arrowhead = none ];
207 -> 84;

208 [label="INSTANCE with matching:\nT1 -> T217\nT2 -> T213", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 208 [arrowhead = none , style=dashed];
208 -> 1[style=dashed];

209 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
84 -> 209 [arrowhead = none ];
209 -> 85;

210 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
84 -> 210 [arrowhead = none ];
210 -> 86;

211 [label="EVAL with clause\nless(0, s(X252)).\nand substitutionT211 -> 0,\nX252 -> T224,\nT214 -> s(T224)", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 211 [arrowhead = none ];
211 -> 87;

212 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 212 [arrowhead = none ];
212 -> 88;

213 [label="EVAL with clause\nless(s(X257), s(X258)) :- less(X257, X258).\nand substitutionX257 -> T229,\nT211 -> s(T229),\nX258 -> T231,\nT214 -> s(T231),\nT230 -> T231", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 213 [arrowhead = none ];
213 -> 90;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 214 [arrowhead = none ];
214 -> 91;

215 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 215 [arrowhead = none ];
215 -> 89;

216 [label="INSTANCE with matching:\nT211 -> T229\nT214 -> T231", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 216 [arrowhead = none , style=dashed];
216 -> 82[style=dashed];

217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
92 -> 217 [arrowhead = none ];
217 -> 94;

218 [label="EVAL with clause\nin(X318, tree(X319, X320, X321)) :- ','(less(X319, X318), in(X318, X321)).\nand substitutionT1 -> T297,\nX318 -> T297,\nX319 -> T294,\nX320 -> T295,\nX321 -> T296,\nT2 -> tree(T294, T295, T296),\nT293 -> T297", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 218 [arrowhead = none ];
218 -> 105;

219 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 219 [arrowhead = none ];
219 -> 106;

220 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
94 -> 220 [arrowhead = none ];
220 -> 95;

221 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
94 -> 221 [arrowhead = none ];
221 -> 96;

222 [label="EVAL with clause\nless(0, s(X279)).\nand substitutionT248 -> 0,\nX279 -> T253,\nT245 -> s(T253)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 222 [arrowhead = none ];
222 -> 97;

223 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 223 [arrowhead = none ];
223 -> 98;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 224 [arrowhead = none ];
224 -> 99;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 225 [arrowhead = none ];
225 -> 100;

226 [label="INSTANCE with matching:\nT15 -> T246", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 226 [arrowhead = none , style=dashed];
226 -> 10[style=dashed];

227 [label="EVAL with clause\nless(s(X294), s(X295)) :- less(X294, X295).\nand substitutionX294 -> T268,\nT248 -> s(T268),\nX295 -> T267,\nT245 -> s(T267),\nT266 -> T268", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 227 [arrowhead = none ];
227 -> 101;

228 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 228 [arrowhead = none ];
228 -> 102;

229 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 229 [arrowhead = none ];
229 -> 103;

230 [label="INSTANCE with matching:\nT89 -> T268\nT88 -> T267\nT15 -> T246", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 230 [arrowhead = none , style=dashed];
230 -> 40[style=dashed];

231 [label="ONLY EVAL with clause\nin(X308, tree(X309, X310, X311)) :- ','(less(X309, X308), in(X308, X311)).\nand substitutionT1 -> T286,\nX308 -> T286,\nT245 -> T283,\nX309 -> T283,\nT246 -> T284,\nX310 -> T284,\nT247 -> T285,\nX311 -> T285,\nT282 -> T286", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 231 [arrowhead = none ];
231 -> 104;

232 [label="INSTANCE with matching:\nT211 -> T283\nT214 -> T286\nT213 -> T285", fontsize=14, style = filled, fillcolor = lightgrey];
104 -> 232 [arrowhead = none , style=dashed];
232 -> 81[style=dashed];

233 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
105 -> 233 [arrowhead = none ];
233 -> 107;

234 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 234 [arrowhead = none ];
234 -> 108;

235 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 235 [arrowhead = none ];
235 -> 109;

236 [label="EVAL with clause\nless(0, s(X326)).\nand substitutionT294 -> 0,\nX326 -> T303,\nT297 -> s(T303),\nT302 -> T303", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 236 [arrowhead = none ];
236 -> 110;

237 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 237 [arrowhead = none ];
237 -> 111;

238 [label="EVAL with clause\nless(s(X337), s(X338)) :- less(X337, X338).\nand substitutionX337 -> T314,\nT294 -> s(T314),\nX338 -> T316,\nT297 -> s(T316),\nT315 -> T316", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 238 [arrowhead = none ];
238 -> 112;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 239 [arrowhead = none ];
239 -> 113;

240 [label="INSTANCE with matching:\nT1 -> s(T303)\nT2 -> T296", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 240 [arrowhead = none , style=dashed];
240 -> 1[style=dashed];

241 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
112 -> 241 [arrowhead = none ];
241 -> 114;

242 [label="SPLIT 2\nnew knowledge:\nT314 is ground\nreplacements:T316 -> T319,\nT1 -> T320", fontsize=14, style = filled, fillcolor = violet];
112 -> 242 [arrowhead = none ];
242 -> 115;

243 [label="INSTANCE with matching:\nT211 -> T314\nT214 -> T316", fontsize=14, style = filled, fillcolor = lightgrey];
114 -> 243 [arrowhead = none , style=dashed];
243 -> 82[style=dashed];

244 [label="INSTANCE with matching:\nT1 -> s(T319)\nT2 -> T296", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 244 [arrowhead = none , style=dashed];
244 -> 1[style=dashed];

}

(2) Obligation:

Triples:

inA(tree(X1, X2, X3)) :- ','(lesscB(X1), inA(X2)).
inA(tree(X1, X2, X3)) :- ','(lesscC(X1), inA(X3)).
lessD(s(X1), s(X2)) :- lessD(X1, X2).
inE(X1, tree(s(X2), X3, X4)) :- lessG(X1, X2).
inE(X1, tree(X2, X3, X4)) :- ','(lesscF(X1, X2), inE(X1, X3)).
inE(X1, tree(X2, X3, X4)) :- lessG(X2, s(X1)).
inE(X1, tree(X2, X3, X4)) :- ','(lesscG(X2, s(X1)), inE(X1, X4)).
lessG(s(X1), s(X2)) :- lessG(X1, X2).
lessK(s(X1), s(X2)) :- lessK(X1, X2).
pI(X1, X2, X3) :- lessD(X1, X2).
pI(X1, X2, X3) :- ','(lesscD(X1, X2), inE(X1, X3)).
pJ(X1, X2, X3) :- lessK(X1, X2).
pJ(X1, X2, X3) :- ','(lesscK(X1, X2), inH(X2, X3)).
inH(0, tree(s(X1), X2, X3)) :- inA(X2).
inH(s(X1), tree(s(X2), X3, X4)) :- pI(X1, X2, X3).
inH(X1, tree(X2, X3, X4)) :- pJ(X2, X1, X4).
inH(0, tree(s(X1), X2, X3)) :- inA(X2).
inH(s(X1), tree(s(X2), X3, X4)) :- pI(X1, X2, X3).
inH(X1, tree(X2, X3, X4)) :- pJ(X2, X1, X4).
inH(s(X1), tree(0, X2, X3)) :- inH(s(X1), X3).
inH(s(X1), tree(s(X2), X3, X4)) :- lessK(X2, X1).
inH(s(X1), tree(s(X2), X3, X4)) :- ','(lesscK(X2, X1), inH(s(X1), X4)).

Clauses:

incA(tree(0, X1, X2)).
incA(tree(X1, X2, X3)) :- ','(lesscB(X1), incA(X2)).
incA(tree(X1, X2, X3)) :- ','(lesscC(X1), incA(X3)).
lesscD(0, s(X1)).
lesscD(s(X1), s(X2)) :- lesscD(X1, X2).
incE(X1, tree(s(X1), X2, X3)).
incE(X1, tree(X2, X3, X4)) :- ','(lesscF(X1, X2), incE(X1, X3)).
incE(X1, tree(X2, X3, X4)) :- ','(lesscG(X2, s(X1)), incE(X1, X4)).
lesscG(0, s(X1)).
lesscG(s(X1), s(X2)) :- lesscG(X1, X2).
incH(X1, tree(X1, X2, X3)).
incH(0, tree(s(X1), X2, X3)) :- incA(X2).
incH(s(X1), tree(s(X2), X3, X4)) :- qcI(X1, X2, X3).
incH(X1, tree(X2, X3, X4)) :- qcJ(X2, X1, X4).
incH(0, tree(s(X1), X2, X3)) :- incA(X2).
incH(s(X1), tree(s(X2), X3, X4)) :- qcI(X1, X2, X3).
incH(X1, tree(X2, X3, X4)) :- qcJ(X2, X1, X4).
incH(s(X1), tree(0, X2, X3)) :- incH(s(X1), X3).
incH(s(X1), tree(s(X2), X3, X4)) :- ','(lesscK(X2, X1), incH(s(X1), X4)).
lesscK(0, s(X1)).
lesscK(s(X1), s(X2)) :- lesscK(X1, X2).
qcI(X1, X2, X3) :- ','(lesscD(X1, X2), incE(X1, X3)).
qcJ(X1, X2, X3) :- ','(lesscK(X1, X2), incH(X2, X3)).
lesscB(s(X1)).
lesscF(X1, s(X2)) :- lesscG(X1, X2).

Afs:

inH(x1, x2)  =  inH(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

inA(tree(X1, X2, X3)) :- ','(lesscB(X1), inA(X2)).
lessD(s(X1), s(X2)) :- lessD(X1, X2).
inE(X1, tree(s(X2), X3, X4)) :- lessG(X1, X2).
inE(X1, tree(X2, X3, X4)) :- ','(lesscF(X1, X2), inE(X1, X3)).
inE(X1, tree(X2, X3, X4)) :- lessG(X2, s(X1)).
inE(X1, tree(X2, X3, X4)) :- ','(lesscG(X2, s(X1)), inE(X1, X4)).
lessG(s(X1), s(X2)) :- lessG(X1, X2).
lessK(s(X1), s(X2)) :- lessK(X1, X2).
pI(X1, X2, X3) :- lessD(X1, X2).
pI(X1, X2, X3) :- ','(lesscD(X1, X2), inE(X1, X3)).
pJ(X1, X2, X3) :- lessK(X1, X2).
pJ(X1, X2, X3) :- ','(lesscK(X1, X2), inH(X2, X3)).
inH(0, tree(s(X1), X2, X3)) :- inA(X2).
inH(s(X1), tree(s(X2), X3, X4)) :- pI(X1, X2, X3).
inH(X1, tree(X2, X3, X4)) :- pJ(X2, X1, X4).
inH(0, tree(s(X1), X2, X3)) :- inA(X2).
inH(s(X1), tree(s(X2), X3, X4)) :- pI(X1, X2, X3).
inH(X1, tree(X2, X3, X4)) :- pJ(X2, X1, X4).
inH(s(X1), tree(0, X2, X3)) :- inH(s(X1), X3).
inH(s(X1), tree(s(X2), X3, X4)) :- lessK(X2, X1).
inH(s(X1), tree(s(X2), X3, X4)) :- ','(lesscK(X2, X1), inH(s(X1), X4)).

Clauses:

incA(tree(0, X1, X2)).
incA(tree(X1, X2, X3)) :- ','(lesscB(X1), incA(X2)).
lesscD(0, s(X1)).
lesscD(s(X1), s(X2)) :- lesscD(X1, X2).
incE(X1, tree(s(X1), X2, X3)).
incE(X1, tree(X2, X3, X4)) :- ','(lesscF(X1, X2), incE(X1, X3)).
incE(X1, tree(X2, X3, X4)) :- ','(lesscG(X2, s(X1)), incE(X1, X4)).
lesscG(0, s(X1)).
lesscG(s(X1), s(X2)) :- lesscG(X1, X2).
incH(X1, tree(X1, X2, X3)).
incH(0, tree(s(X1), X2, X3)) :- incA(X2).
incH(s(X1), tree(s(X2), X3, X4)) :- qcI(X1, X2, X3).
incH(X1, tree(X2, X3, X4)) :- qcJ(X2, X1, X4).
incH(0, tree(s(X1), X2, X3)) :- incA(X2).
incH(s(X1), tree(s(X2), X3, X4)) :- qcI(X1, X2, X3).
incH(X1, tree(X2, X3, X4)) :- qcJ(X2, X1, X4).
incH(s(X1), tree(0, X2, X3)) :- incH(s(X1), X3).
incH(s(X1), tree(s(X2), X3, X4)) :- ','(lesscK(X2, X1), incH(s(X1), X4)).
lesscK(0, s(X1)).
lesscK(s(X1), s(X2)) :- lesscK(X1, X2).
qcI(X1, X2, X3) :- ','(lesscD(X1, X2), incE(X1, X3)).
qcJ(X1, X2, X3) :- ','(lesscK(X1, X2), incH(X2, X3)).
lesscB(s(X1)).
lesscF(X1, s(X2)) :- lesscG(X1, X2).

Afs:

inH(x1, x2)  =  inH(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
inH_in: (f,b)
inA_in: (b)
pI_in: (f,b,b)
lessD_in: (f,b)
lesscD_in: (f,b)
inE_in: (b,b)
lessG_in: (b,b)
lesscF_in: (b,b)
lesscG_in: (b,b)
pJ_in: (b,f,b)
lessK_in: (b,f)
lesscK_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

INH_IN_AG(0, tree(s(X1), X2, X3)) → U18_AG(X1, X2, X3, inA_in_g(X2))
INH_IN_AG(0, tree(s(X1), X2, X3)) → INA_IN_G(X2)
INA_IN_G(tree(X1, X2, X3)) → U1_G(X1, X2, X3, lesscB_in_g(X1))
U1_G(X1, X2, X3, lesscB_out_g(X1)) → U2_G(X1, X2, X3, inA_in_g(X2))
U1_G(X1, X2, X3, lesscB_out_g(X1)) → INA_IN_G(X2)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U19_AG(X1, X2, X3, X4, pI_in_agg(X1, X2, X3))
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → PI_IN_AGG(X1, X2, X3)
PI_IN_AGG(X1, X2, X3) → U12_AGG(X1, X2, X3, lessD_in_ag(X1, X2))
PI_IN_AGG(X1, X2, X3) → LESSD_IN_AG(X1, X2)
LESSD_IN_AG(s(X1), s(X2)) → U3_AG(X1, X2, lessD_in_ag(X1, X2))
LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)
PI_IN_AGG(X1, X2, X3) → U13_AGG(X1, X2, X3, lesscD_in_ag(X1, X2))
U13_AGG(X1, X2, X3, lesscD_out_ag(X1, X2)) → U14_AGG(X1, X2, X3, inE_in_gg(X1, X3))
U13_AGG(X1, X2, X3, lesscD_out_ag(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(s(X2), X3, X4)) → U4_GG(X1, X2, X3, X4, lessG_in_gg(X1, X2))
INE_IN_GG(X1, tree(s(X2), X3, X4)) → LESSG_IN_GG(X1, X2)
LESSG_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessG_in_gg(X1, X2))
LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)
INE_IN_GG(X1, tree(X2, X3, X4)) → U5_GG(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → U6_GG(X1, X2, X3, X4, inE_in_gg(X1, X3))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(X2, X3, X4)) → U7_GG(X1, X2, X3, X4, lessG_in_gg(X2, s(X1)))
INE_IN_GG(X1, tree(X2, X3, X4)) → LESSG_IN_GG(X2, s(X1))
INE_IN_GG(X1, tree(X2, X3, X4)) → U8_GG(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → U9_GG(X1, X2, X3, X4, inE_in_gg(X1, X4))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INE_IN_GG(X1, X4)
INH_IN_AG(X1, tree(X2, X3, X4)) → U20_AG(X1, X2, X3, X4, pJ_in_gag(X2, X1, X4))
INH_IN_AG(X1, tree(X2, X3, X4)) → PJ_IN_GAG(X2, X1, X4)
PJ_IN_GAG(X1, X2, X3) → U15_GAG(X1, X2, X3, lessK_in_ga(X1, X2))
PJ_IN_GAG(X1, X2, X3) → LESSK_IN_GA(X1, X2)
LESSK_IN_GA(s(X1), s(X2)) → U11_GA(X1, X2, lessK_in_ga(X1, X2))
LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)
PJ_IN_GAG(X1, X2, X3) → U16_GAG(X1, X2, X3, lesscK_in_ga(X1, X2))
U16_GAG(X1, X2, X3, lesscK_out_ga(X1, X2)) → U17_GAG(X1, X2, X3, inH_in_ag(X2, X3))
U16_GAG(X1, X2, X3, lesscK_out_ga(X1, X2)) → INH_IN_AG(X2, X3)
INH_IN_AG(s(X1), tree(0, X2, X3)) → U21_AG(X1, X2, X3, inH_in_ag(s(X1), X3))
INH_IN_AG(s(X1), tree(0, X2, X3)) → INH_IN_AG(s(X1), X3)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U22_AG(X1, X2, X3, X4, lessK_in_ga(X2, X1))
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → LESSK_IN_GA(X2, X1)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U23_AG(X1, X2, X3, X4, lesscK_in_ga(X2, X1))
U23_AG(X1, X2, X3, X4, lesscK_out_ga(X2, X1)) → U24_AG(X1, X2, X3, X4, inH_in_ag(s(X1), X4))
U23_AG(X1, X2, X3, X4, lesscK_out_ga(X2, X1)) → INH_IN_AG(s(X1), X4)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
inH_in_ag(x1, x2)  =  inH_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
inA_in_g(x1)  =  inA_in_g(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
pI_in_agg(x1, x2, x3)  =  pI_in_agg(x2, x3)
lessD_in_ag(x1, x2)  =  lessD_in_ag(x2)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
inE_in_gg(x1, x2)  =  inE_in_gg(x1, x2)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
pJ_in_gag(x1, x2, x3)  =  pJ_in_gag(x1, x3)
lessK_in_ga(x1, x2)  =  lessK_in_ga(x1)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INH_IN_AG(x1, x2)  =  INH_IN_AG(x2)
U18_AG(x1, x2, x3, x4)  =  U18_AG(x1, x2, x3, x4)
INA_IN_G(x1)  =  INA_IN_G(x1)
U1_G(x1, x2, x3, x4)  =  U1_G(x1, x2, x3, x4)
U2_G(x1, x2, x3, x4)  =  U2_G(x1, x2, x3, x4)
U19_AG(x1, x2, x3, x4, x5)  =  U19_AG(x2, x3, x4, x5)
PI_IN_AGG(x1, x2, x3)  =  PI_IN_AGG(x2, x3)
U12_AGG(x1, x2, x3, x4)  =  U12_AGG(x2, x3, x4)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U13_AGG(x1, x2, x3, x4)  =  U13_AGG(x2, x3, x4)
U14_AGG(x1, x2, x3, x4)  =  U14_AGG(x1, x2, x3, x4)
INE_IN_GG(x1, x2)  =  INE_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4, x5)  =  U4_GG(x1, x2, x3, x4, x5)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U5_GG(x1, x2, x3, x4, x5)  =  U5_GG(x1, x2, x3, x4, x5)
U6_GG(x1, x2, x3, x4, x5)  =  U6_GG(x1, x2, x3, x4, x5)
U7_GG(x1, x2, x3, x4, x5)  =  U7_GG(x1, x2, x3, x4, x5)
U8_GG(x1, x2, x3, x4, x5)  =  U8_GG(x1, x2, x3, x4, x5)
U9_GG(x1, x2, x3, x4, x5)  =  U9_GG(x1, x2, x3, x4, x5)
U20_AG(x1, x2, x3, x4, x5)  =  U20_AG(x2, x3, x4, x5)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U15_GAG(x1, x2, x3, x4)  =  U15_GAG(x1, x3, x4)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U16_GAG(x1, x2, x3, x4)  =  U16_GAG(x1, x3, x4)
U17_GAG(x1, x2, x3, x4)  =  U17_GAG(x1, x3, x4)
U21_AG(x1, x2, x3, x4)  =  U21_AG(x2, x3, x4)
U22_AG(x1, x2, x3, x4, x5)  =  U22_AG(x2, x3, x4, x5)
U23_AG(x1, x2, x3, x4, x5)  =  U23_AG(x2, x3, x4, x5)
U24_AG(x1, x2, x3, x4, x5)  =  U24_AG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INH_IN_AG(0, tree(s(X1), X2, X3)) → U18_AG(X1, X2, X3, inA_in_g(X2))
INH_IN_AG(0, tree(s(X1), X2, X3)) → INA_IN_G(X2)
INA_IN_G(tree(X1, X2, X3)) → U1_G(X1, X2, X3, lesscB_in_g(X1))
U1_G(X1, X2, X3, lesscB_out_g(X1)) → U2_G(X1, X2, X3, inA_in_g(X2))
U1_G(X1, X2, X3, lesscB_out_g(X1)) → INA_IN_G(X2)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U19_AG(X1, X2, X3, X4, pI_in_agg(X1, X2, X3))
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → PI_IN_AGG(X1, X2, X3)
PI_IN_AGG(X1, X2, X3) → U12_AGG(X1, X2, X3, lessD_in_ag(X1, X2))
PI_IN_AGG(X1, X2, X3) → LESSD_IN_AG(X1, X2)
LESSD_IN_AG(s(X1), s(X2)) → U3_AG(X1, X2, lessD_in_ag(X1, X2))
LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)
PI_IN_AGG(X1, X2, X3) → U13_AGG(X1, X2, X3, lesscD_in_ag(X1, X2))
U13_AGG(X1, X2, X3, lesscD_out_ag(X1, X2)) → U14_AGG(X1, X2, X3, inE_in_gg(X1, X3))
U13_AGG(X1, X2, X3, lesscD_out_ag(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(s(X2), X3, X4)) → U4_GG(X1, X2, X3, X4, lessG_in_gg(X1, X2))
INE_IN_GG(X1, tree(s(X2), X3, X4)) → LESSG_IN_GG(X1, X2)
LESSG_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessG_in_gg(X1, X2))
LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)
INE_IN_GG(X1, tree(X2, X3, X4)) → U5_GG(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → U6_GG(X1, X2, X3, X4, inE_in_gg(X1, X3))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(X2, X3, X4)) → U7_GG(X1, X2, X3, X4, lessG_in_gg(X2, s(X1)))
INE_IN_GG(X1, tree(X2, X3, X4)) → LESSG_IN_GG(X2, s(X1))
INE_IN_GG(X1, tree(X2, X3, X4)) → U8_GG(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → U9_GG(X1, X2, X3, X4, inE_in_gg(X1, X4))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INE_IN_GG(X1, X4)
INH_IN_AG(X1, tree(X2, X3, X4)) → U20_AG(X1, X2, X3, X4, pJ_in_gag(X2, X1, X4))
INH_IN_AG(X1, tree(X2, X3, X4)) → PJ_IN_GAG(X2, X1, X4)
PJ_IN_GAG(X1, X2, X3) → U15_GAG(X1, X2, X3, lessK_in_ga(X1, X2))
PJ_IN_GAG(X1, X2, X3) → LESSK_IN_GA(X1, X2)
LESSK_IN_GA(s(X1), s(X2)) → U11_GA(X1, X2, lessK_in_ga(X1, X2))
LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)
PJ_IN_GAG(X1, X2, X3) → U16_GAG(X1, X2, X3, lesscK_in_ga(X1, X2))
U16_GAG(X1, X2, X3, lesscK_out_ga(X1, X2)) → U17_GAG(X1, X2, X3, inH_in_ag(X2, X3))
U16_GAG(X1, X2, X3, lesscK_out_ga(X1, X2)) → INH_IN_AG(X2, X3)
INH_IN_AG(s(X1), tree(0, X2, X3)) → U21_AG(X1, X2, X3, inH_in_ag(s(X1), X3))
INH_IN_AG(s(X1), tree(0, X2, X3)) → INH_IN_AG(s(X1), X3)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U22_AG(X1, X2, X3, X4, lessK_in_ga(X2, X1))
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → LESSK_IN_GA(X2, X1)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U23_AG(X1, X2, X3, X4, lesscK_in_ga(X2, X1))
U23_AG(X1, X2, X3, X4, lesscK_out_ga(X2, X1)) → U24_AG(X1, X2, X3, X4, inH_in_ag(s(X1), X4))
U23_AG(X1, X2, X3, X4, lesscK_out_ga(X2, X1)) → INH_IN_AG(s(X1), X4)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
inH_in_ag(x1, x2)  =  inH_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
inA_in_g(x1)  =  inA_in_g(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
pI_in_agg(x1, x2, x3)  =  pI_in_agg(x2, x3)
lessD_in_ag(x1, x2)  =  lessD_in_ag(x2)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
inE_in_gg(x1, x2)  =  inE_in_gg(x1, x2)
lessG_in_gg(x1, x2)  =  lessG_in_gg(x1, x2)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
pJ_in_gag(x1, x2, x3)  =  pJ_in_gag(x1, x3)
lessK_in_ga(x1, x2)  =  lessK_in_ga(x1)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INH_IN_AG(x1, x2)  =  INH_IN_AG(x2)
U18_AG(x1, x2, x3, x4)  =  U18_AG(x1, x2, x3, x4)
INA_IN_G(x1)  =  INA_IN_G(x1)
U1_G(x1, x2, x3, x4)  =  U1_G(x1, x2, x3, x4)
U2_G(x1, x2, x3, x4)  =  U2_G(x1, x2, x3, x4)
U19_AG(x1, x2, x3, x4, x5)  =  U19_AG(x2, x3, x4, x5)
PI_IN_AGG(x1, x2, x3)  =  PI_IN_AGG(x2, x3)
U12_AGG(x1, x2, x3, x4)  =  U12_AGG(x2, x3, x4)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U13_AGG(x1, x2, x3, x4)  =  U13_AGG(x2, x3, x4)
U14_AGG(x1, x2, x3, x4)  =  U14_AGG(x1, x2, x3, x4)
INE_IN_GG(x1, x2)  =  INE_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4, x5)  =  U4_GG(x1, x2, x3, x4, x5)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U5_GG(x1, x2, x3, x4, x5)  =  U5_GG(x1, x2, x3, x4, x5)
U6_GG(x1, x2, x3, x4, x5)  =  U6_GG(x1, x2, x3, x4, x5)
U7_GG(x1, x2, x3, x4, x5)  =  U7_GG(x1, x2, x3, x4, x5)
U8_GG(x1, x2, x3, x4, x5)  =  U8_GG(x1, x2, x3, x4, x5)
U9_GG(x1, x2, x3, x4, x5)  =  U9_GG(x1, x2, x3, x4, x5)
U20_AG(x1, x2, x3, x4, x5)  =  U20_AG(x2, x3, x4, x5)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U15_GAG(x1, x2, x3, x4)  =  U15_GAG(x1, x3, x4)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U16_GAG(x1, x2, x3, x4)  =  U16_GAG(x1, x3, x4)
U17_GAG(x1, x2, x3, x4)  =  U17_GAG(x1, x3, x4)
U21_AG(x1, x2, x3, x4)  =  U21_AG(x2, x3, x4)
U22_AG(x1, x2, x3, x4, x5)  =  U22_AG(x2, x3, x4, x5)
U23_AG(x1, x2, x3, x4, x5)  =  U23_AG(x2, x3, x4, x5)
U24_AG(x1, x2, x3, x4, x5)  =  U24_AG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 27 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSK_IN_GA(s(X1), s(X2)) → LESSK_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSK_IN_GA(x1, x2)  =  LESSK_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSK_IN_GA(s(X1)) → LESSK_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSK_IN_GA(s(X1)) → LESSK_IN_GA(X1)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
LESSG_IN_GG(x1, x2)  =  LESSG_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSG_IN_GG(s(X1), s(X2)) → LESSG_IN_GG(X1, X2)
  The graph contains the following edges 1 > 1, 2 > 2

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INE_IN_GG(X1, tree(X2, X3, X4)) → U5_GG(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(X2, X3, X4)) → U8_GG(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INE_IN_GG(X1, X4)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INE_IN_GG(x1, x2)  =  INE_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4, x5)  =  U5_GG(x1, x2, x3, x4, x5)
U8_GG(x1, x2, x3, x4, x5)  =  U8_GG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INE_IN_GG(X1, tree(X2, X3, X4)) → U5_GG(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(X2, X3, X4)) → U8_GG(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INE_IN_GG(X1, X4)

The TRS R consists of the following rules:

lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INE_IN_GG(X1, tree(X2, X3, X4)) → U5_GG(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INE_IN_GG(X1, X3)
INE_IN_GG(X1, tree(X2, X3, X4)) → U8_GG(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INE_IN_GG(X1, X4)

The TRS R consists of the following rules:

lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lesscF_in_gg(x0, x1)
lesscG_in_gg(x0, x1)
U45_gg(x0, x1, x2)
U33_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• U5_GG(X1, X2, X3, X4, lesscF_out_gg(X1, X2)) → INE_IN_GG(X1, X3)
  The graph contains the following edges 1 >= 1, 5 > 1, 3 >= 2

• U8_GG(X1, X2, X3, X4, lesscG_out_gg(X2, s(X1))) → INE_IN_GG(X1, X4)
  The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2

• INE_IN_GG(X1, tree(X2, X3, X4)) → U5_GG(X1, X2, X3, X4, lesscF_in_gg(X1, X2))
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

• INE_IN_GG(X1, tree(X2, X3, X4)) → U8_GG(X1, X2, X3, X4, lesscG_in_gg(X2, s(X1)))
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSD_IN_AG(s(X1), s(X2)) → LESSD_IN_AG(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSD_IN_AG(x1, x2)  =  LESSD_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSD_IN_AG(s(X2)) → LESSD_IN_AG(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSD_IN_AG(s(X2)) → LESSD_IN_AG(X2)
  The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U1_G(X1, X2, X3, lesscB_out_g(X1)) → INA_IN_G(X2)
INA_IN_G(tree(X1, X2, X3)) → U1_G(X1, X2, X3, lesscB_in_g(X1))

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INA_IN_G(x1)  =  INA_IN_G(x1)
U1_G(x1, x2, x3, x4)  =  U1_G(x1, x2, x3, x4)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

U1_G(X1, X2, X3, lesscB_out_g(X1)) → INA_IN_G(X2)
INA_IN_G(tree(X1, X2, X3)) → U1_G(X1, X2, X3, lesscB_in_g(X1))

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U1_G(X1, X2, X3, lesscB_out_g(X1)) → INA_IN_G(X2)
INA_IN_G(tree(X1, X2, X3)) → U1_G(X1, X2, X3, lesscB_in_g(X1))

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))

The set Q consists of the following terms:

lesscB_in_g(x0)

We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• INA_IN_G(tree(X1, X2, X3)) → U1_G(X1, X2, X3, lesscB_in_g(X1))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• U1_G(X1, X2, X3, lesscB_out_g(X1)) → INA_IN_G(X2)
  The graph contains the following edges 2 >= 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INH_IN_AG(X1, tree(X2, X3, X4)) → PJ_IN_GAG(X2, X1, X4)
PJ_IN_GAG(X1, X2, X3) → U16_GAG(X1, X2, X3, lesscK_in_ga(X1, X2))
U16_GAG(X1, X2, X3, lesscK_out_ga(X1, X2)) → INH_IN_AG(X2, X3)
INH_IN_AG(s(X1), tree(0, X2, X3)) → INH_IN_AG(s(X1), X3)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U23_AG(X1, X2, X3, X4, lesscK_in_ga(X2, X1))
U23_AG(X1, X2, X3, X4, lesscK_out_ga(X2, X1)) → INH_IN_AG(s(X1), X4)

The TRS R consists of the following rules:

lesscB_in_g(s(X1)) → lesscB_out_g(s(X1))
lesscD_in_ag(0, s(X1)) → lesscD_out_ag(0, s(X1))
lesscD_in_ag(s(X1), s(X2)) → U28_ag(X1, X2, lesscD_in_ag(X1, X2))
U28_ag(X1, X2, lesscD_out_ag(X1, X2)) → lesscD_out_ag(s(X1), s(X2))
lesscF_in_gg(X1, s(X2)) → U45_gg(X1, X2, lesscG_in_gg(X1, X2))
lesscG_in_gg(0, s(X1)) → lesscG_out_gg(0, s(X1))
lesscG_in_gg(s(X1), s(X2)) → U33_gg(X1, X2, lesscG_in_gg(X1, X2))
U33_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscG_out_gg(s(X1), s(X2))
U45_gg(X1, X2, lesscG_out_gg(X1, X2)) → lesscF_out_gg(X1, s(X2))
lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_g(x1)  =  lesscB_in_g(x1)
lesscB_out_g(x1)  =  lesscB_out_g(x1)
lesscD_in_ag(x1, x2)  =  lesscD_in_ag(x2)
lesscD_out_ag(x1, x2)  =  lesscD_out_ag(x1, x2)
U28_ag(x1, x2, x3)  =  U28_ag(x2, x3)
lesscF_in_gg(x1, x2)  =  lesscF_in_gg(x1, x2)
U45_gg(x1, x2, x3)  =  U45_gg(x1, x2, x3)
lesscG_in_gg(x1, x2)  =  lesscG_in_gg(x1, x2)
0  =  0
lesscG_out_gg(x1, x2)  =  lesscG_out_gg(x1, x2)
U33_gg(x1, x2, x3)  =  U33_gg(x1, x2, x3)
lesscF_out_gg(x1, x2)  =  lesscF_out_gg(x1, x2)
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INH_IN_AG(x1, x2)  =  INH_IN_AG(x2)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U16_GAG(x1, x2, x3, x4)  =  U16_GAG(x1, x3, x4)
U23_AG(x1, x2, x3, x4, x5)  =  U23_AG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

INH_IN_AG(X1, tree(X2, X3, X4)) → PJ_IN_GAG(X2, X1, X4)
PJ_IN_GAG(X1, X2, X3) → U16_GAG(X1, X2, X3, lesscK_in_ga(X1, X2))
U16_GAG(X1, X2, X3, lesscK_out_ga(X1, X2)) → INH_IN_AG(X2, X3)
INH_IN_AG(s(X1), tree(0, X2, X3)) → INH_IN_AG(s(X1), X3)
INH_IN_AG(s(X1), tree(s(X2), X3, X4)) → U23_AG(X1, X2, X3, X4, lesscK_in_ga(X2, X1))
U23_AG(X1, X2, X3, X4, lesscK_out_ga(X2, X1)) → INH_IN_AG(s(X1), X4)

The TRS R consists of the following rules:

lesscK_in_ga(0, s(X1)) → lesscK_out_ga(0, s(X1))
lesscK_in_ga(s(X1), s(X2)) → U40_ga(X1, X2, lesscK_in_ga(X1, X2))
U40_ga(X1, X2, lesscK_out_ga(X1, X2)) → lesscK_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lesscK_in_ga(x1, x2)  =  lesscK_in_ga(x1)
lesscK_out_ga(x1, x2)  =  lesscK_out_ga(x1)
U40_ga(x1, x2, x3)  =  U40_ga(x1, x3)
INH_IN_AG(x1, x2)  =  INH_IN_AG(x2)
PJ_IN_GAG(x1, x2, x3)  =  PJ_IN_GAG(x1, x3)
U16_GAG(x1, x2, x3, x4)  =  U16_GAG(x1, x3, x4)
U23_AG(x1, x2, x3, x4, x5)  =  U23_AG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INH_IN_AG(tree(X2, X3, X4)) → PJ_IN_GAG(X2, X4)
PJ_IN_GAG(X1, X3) → U16_GAG(X1, X3, lesscK_in_ga(X1))
U16_GAG(X1, X3, lesscK_out_ga(X1)) → INH_IN_AG(X3)
INH_IN_AG(tree(0, X2, X3)) → INH_IN_AG(X3)
INH_IN_AG(tree(s(X2), X3, X4)) → U23_AG(X2, X3, X4, lesscK_in_ga(X2))
U23_AG(X2, X3, X4, lesscK_out_ga(X2)) → INH_IN_AG(X4)

The TRS R consists of the following rules:

lesscK_in_ga(0) → lesscK_out_ga(0)
lesscK_in_ga(s(X1)) → U40_ga(X1, lesscK_in_ga(X1))
U40_ga(X1, lesscK_out_ga(X1)) → lesscK_out_ga(s(X1))

The set Q consists of the following terms:

lesscK_in_ga(x0)
U40_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• PJ_IN_GAG(X1, X3) → U16_GAG(X1, X3, lesscK_in_ga(X1))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U16_GAG(X1, X3, lesscK_out_ga(X1)) → INH_IN_AG(X3)
  The graph contains the following edges 2 >= 1

• INH_IN_AG(tree(X2, X3, X4)) → PJ_IN_GAG(X2, X4)
  The graph contains the following edges 1 > 1, 1 > 2

• INH_IN_AG(tree(s(X2), X3, X4)) → U23_AG(X2, X3, X4, lesscK_in_ga(X2))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

• INH_IN_AG(tree(0, X2, X3)) → INH_IN_AG(X3)
  The graph contains the following edges 1 > 1

• U23_AG(X2, X3, X4, lesscK_out_ga(X2)) → INH_IN_AG(X4)
  The graph contains the following edges 3 >= 1

(50) YES